COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002
C00010 ENDMK
C⊗;


function fact
(1 0)
(x y)
 Nat(x true).
 Nat(y true) ∧ >(y 0 true).
  fact(0 1)
	fact(x y) ← %fsub1(x x1), fact(x1 y1), %f*(x y1 y).

type Nat
 Nat(x true) ← Integer(x true), ≥(x 0 true).

generic add
 (x y z)
	(1 1 0)
 %f+
(1 0 1)
 add-2
 Integer(x) ∧ Integer(z).
 Integer(y).
 sub-2
	(0 1 1)
 add-1
 Integer(y) ∧ Integer(z).
 Integer(z).
 sub-1
  .
add(x y z) ← %f-(z x y).

add(x y z) ← %f-(z y x).


generic imult
 (x y z)
(1 1 0)
 %f*
	(0 1 1)
 imult-1
 Integer(y) ∧ Integer(z).
 Integer(x).
 idiv-1
	(1 0 1)
 imult-2
 Integer(x) ∧ Integer(z).
 Integer(y).
 idiv-2
.
imult(0 x 0)
imult(undef 0 x) ← ≠(x 0)
imult(x y z) ← %f//(z y x), %f*(x y z).

imult(x 0 0)
imult(0 undef x) ← ≠(x 0)
imult(x y z) ← %f//(z x y), imult(x y z).


function gcd
 (1 1 0)
 (x y z)
 Nat(x true) ∧ Nat(y true).
 Nat(z true).
 gcd(0 0 undef)
	gcd(0 x x)
	gcd(x 0 x)
	gcd(x y z) ← ≥(x y), add(y w x), gcd(w y z)
	gcd(x y z) ← ≥(y x), add(x w y), gcd(x w z).
	

generic factor
 (w n p r)
	(0 1 1 1)
 factor-1
 Nat(n true) ∧ Nat(p true) ∧ Nat(r true).
 Nat(w true).
 mult-out
	(1 1 0 0)
 factor-34
 Nat(w true) ∧ Nat(n true).
 Nat(p true) ∧ Nat(r true).
 ss-factor
.
factor(r n 0 r) ← gcd(r n 1)
factor(w n p r) ← imult(n r x), %fsub1(p p1), factor(w n p1 x).

factor(w n 0 w) ← <(w n)
factor(w n 0 w) ← gcd(w n 1)
factor(w n p r) ← ≥(w n), imult(v n w), factor(v n p1 r), add(p1 1 p).


generic E
 (x n y z)
	(1 1 1 0)
 E-4
 Nat(x true) ∧ Nat(n true) ∧ Nat(y true).
 Nat(z true).
 ebod-4
	(1 1 0 1)
 E-3
 Nat(x true) ∧ Nat(n true) ∧ Nat(z true).
 Nat(y true).
 ebod-3
	(0 1 1 1)
 E-1
 Nat(y true) ∧ Nat(n true) ∧ Nat(z true).
 Nat(x true).
 ebod-1
.
E(0 n y 0) ← ≠(y 0)
E(x n 0 1) ← ≠(x 0)
E(1 n y 1)
E(x n y z) ← factor(x n p r), imult(p y q), add(n 1 n1), E(r n1 y s), factor(z n q s).

E(x n 0 1) ← ≠(x 0)
E(x n y z) ← factor(x n p r), add(n 1 n1), factor(z n q s), imult(p y q), E(r n1 y s).

E(0 n y 0) ← ≠(y 0)
E(1 n y 1)
E(x n y z) ← factor(z n q s), imult(p y q), add(n 1 n1), E(r n1 y s), factor(x n p r).


generic exp 
 (x y z)
	(1 1 0)
 exp-3
 Nat(x) ∧ Nat(y).
 Nat(z).
 expo
	(1 0 1)
 exp-2
 Nat(x) ∧ Nat(z).
 Nat(y).
 expo
	(0 1 1)
 exp-1
 Nat(z) ∧ Nat(y).
 Nat(x).
 expo
.
exp(x y z) ← E(x 2 y z).



type is-set
is-set('mt-set,true)
is-set( add-elem(x,s), true) ← is-set(s, true), set-mem(x, s, false).


function set-mem
(1 1 0)
(x y z)
is-set(y, true).
boolean(z, true).
set-mem(x, 'mt-set, false)
set-mem(x, add-elem(x, s), true)
set-mem(x, add-elem(y, s), true) ← set-mem(x, s, true)
set-mem(x, add-elem(y, s), false) ← same(x, y, z), same(z, false, true), 
					set-mem(x, s, false).

function same
(1 1 0)

same(x x true)
same(x y false).


function union
(1 1 0)
(x y z)
is-set(x, true) ∧ is-set(y,true).
is-set(z, true).
union('mt-set, y, y)
union(x, 'mt-set, x)
union(add-elem(x,s), y, add-elem(x,z)) ←  set-mem(x, y, false), union(s, y, z)
union(add-elem(x,s), y, z) ← set-mem(x, y, true), union(s, y, z).

.